| Definitions | x:A  B(x),  b, ES, Type, x:A  B(x), AbsInterface(A), left + right,  , {x:A| B(x)} , sys-antecedent(es;Sys), type List,  x:A. B(x), P  Q,  A, P   Q,  x:A. B(x), s = t, P & Q, hd(l), L1  L2, adjacent(T;L;x;y), (x  l), no_repeats(T;l), chain-consistent(f;chain), E(X), (e <loc e'), e  loc e' , case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , !Void(), a:A fp B(a), loc(e), <a, b>, Id, t T, strong-subtype(A;B), X(e), f(a), e  X, Top, let x,y = A in B(x;y), t.1, E,  , True,  T, Dec(P), b | a, a ~ b, a b, a <p b, a < b, A c B, x f y, xL. P(x), (xL.P(x)), r s, r < s, q-rel(r;x), Outcome, l_disjoint(T;l1;l2), (e < e'), e c e', e<e'.P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e[e1,e2).P(e), e[e1,e2).P(e), e[e1,e2].P(e), e[e1,e2].P(e), e(e1,e2].P(e), SqStable(P), P  Q, a =!x:T. Q(x), InvFuns(A;B;f;g), Inj(A;B;f), IsEqFun(T;eq), Refl(T;x,y.E(x;y)), Sym(T;x,y.E(x;y)), Trans(T;x,y.E(x;y)), AntiSym(T;x,y.R(x;y)), Connex(T;x,y.R(x;y)), CoPrime(a,b), Ident(T;op;id), Assoc(T;op), Comm(T;op), Inverse(T;op;id;inv), BiLinear(T;pl;tm), IsBilinear(A;B;C;+a;+b;+c;f), IsAction(A;x;e;S;f), Dist1op2opLR(A;1op;2op), fun_thru_1op(A;B;opa;opb;f), FunThru2op(A;B;opa;opb;f), Cancel(T;S;op), monot(T;x,y.R(x;y);f), IsMonoid(T;op;id), IsGroup(T;op;id;inv), IsMonHom{M1,M2}(f), a b, IsIntegDom(r), IsPrimeIdeal(R;P), f g, EState(T),  , EqDecider(T), Unit, IdLnk, EOrderAxioms(E; pred?; info), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M),  , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', constant_function(f;A;B), SWellFounded(R(x;y)), pred!(e;e'),   x,y. t(x;y),  x:A.B(x), S T, suptype(S; T), first(e), pred(e), x.A(x), x. t(x), Atom$n, a = b, P Q, x dom(f), False, f(x)?z, a < b, ||as||, A B, i j < k,  , {i..j }, #$n, l[i], increasing(f;k), ff, inr x , tt, inl x , x before y l, s ~ t, {T}, SQType(T), b, isrcv(e), kind(e), es-first-from(es;e;l;tg), isrcv(k), lastchange(x;e), (last change to x before e), p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, a < b, [d], eq_atom$n(x;y), q_le(r;s), q_less(a;b), qeq(r;s), a = b, deq-member(eq;x;L), e = e', p q, p q, p q, last(L) |
| Lemmas | before-hd, bool cases, eqtt to assert, bool sq, iff transitivity, eqff to assert, assert of bnot, es-isrcv-loc, guard wf, es-le-loc, bnot wf, Id sq, hd wf, adjacent-sublist, true wf, btrue wf, bfalse wf, sublist weakening, increasing wf, length wf nat, select wf, int seg wf, length wf1, le wf, sublist wf, not functionality wrt iff, iff wf, rev implies wf, assert-eq-id, eq id wf, false wf, es-E-interface-subtype rel, es-interface-val wf2, es-locl wf, es-le wf, chain-consistent wf, es-causle wf, sys-antecedent wf, es-interface wf, deq wf, EOrderAxioms wf, kind wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, bool wf, Knd wf, kindcase wf, IdLnk wf, constant function wf, loc wf, not wf, first wf, top wf, unit wf, pred! wf, strongwellfounded wf, rationals wf, EState wf, event system wf, es-is-interface wf, member wf, es-E wf, es-E-interface wf, subtype rel wf, sq stable from decidable, decidable assert, assert wf, Id wf, es-loc wf |
